$\forall$$T$:Type, $l_{1}$:$T$ List, $v$:$T$, $l_{2}$:$T$ List.
\\[0ex]$l_{1}$ $\leq$ $l_{2}$ $\Rightarrow$ $\parallel$$l_{1}$$\parallel<\parallel$$l_{2}$$\parallel$ \& $l_{2}$[$\parallel$$l_{1}$$\parallel$] $=$ $v$ $\Rightarrow$ $l_{1}$ @ [$v$] $\leq$ $l_{2}$